(set-info :smt-lib-version 2.6)
(set-logic QF_UFNRA)
(set-info :source |
    Simple airplane collision avoidance system model
    Submitted by Tim King (taking@cs.nyu.edu) and Clark Barrett (barrett@cs.nyu.edu)
  |)
(set-info :category "industrial")
(set-info :status sat)
(set-info :difficulty | unknown |)
(declare-fun rrm () Real)
(declare-fun intr_target_alt () Real)
(declare-fun own_target_alt () Real)
(declare-fun intr_alt_rate_mag () Real)
(declare-fun own_alt_rate_mag () Real)
(declare-fun TCA () Real)
(declare-fun MAX_Tau_To_Trigger_Threat () Real)
(declare-fun range (Real) Real)
(declare-fun range_rate (Real) Real)
(declare-fun intr_alt (Real) Real)
(declare-fun intr_alt_rate (Real) Real)
(declare-fun own_alt (Real) Real)
(declare-fun own_alt_rate (Real) Real)
(declare-fun alt_proj (Real) Real)
(declare-fun limited_alt_proj (Real) Real)
(declare-fun state_is_No_RA (Real) Bool)
(declare-fun state_is_Climb (Real) Bool)
(declare-fun state_is_Descend (Real) Bool)
(declare-fun Collision_Threat (Real) Bool)
(declare-fun tau (Real) Real)
(assert (let ((?v_1 (own_alt 0)) (?v_7 (state_is_No_RA 0)) (?v_23 (Collision_Threat 0)) (?v_0 (range_rate 0)) (?v_2 (own_alt_rate 0)) (?v_3 (intr_alt 0)) (?v_4 (intr_alt_rate 0)) (?v_15 (range 0)) (?v_8 (state_is_Climb 0))) (let ((?v_10 (not ?v_8)) (?v_11 (state_is_Descend 0))) (let ((?v_9 (not ?v_11)) (?v_12 (not ?v_7)) (?v_14 (tau 0))) (let ((?v_17 (* ?v_14 ?v_4)) (?v_18 (* ?v_14 ?v_2))) (let ((?v_22 (* 1 ?v_18)) (?v_19 (* 1 ?v_17)) (?v_6 (* (- 1) ?v_1)) (?v_24 (* (- 1) own_target_alt)) (?v_5 (* (- 1) ?v_3)) (?v_13 (* (- 1) ?v_15)) (?v_16 (* (- 1) ?v_0)) (?v_21 (* (- 1) ?v_17)) (?v_20 (* (- 1) ?v_18))) (and (= ?v_1 15000) (and ?v_7 (not ?v_23) (= (range TCA) 0) (= (tau TCA) 0) (ite (< 0 TCA) (= (+ 0 ?v_0 rrm) 0) (= ?v_0 rrm)) (ite (< 0 (+ 0 ?v_6 own_target_alt)) (= ?v_2 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_1 ?v_24)) (= (+ 0 ?v_2 own_alt_rate_mag) 0) (= ?v_2 0))) (ite (< 0 (+ 0 ?v_5 intr_target_alt)) (= ?v_4 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_3 (* (- 1) intr_target_alt))) (= (+ 0 ?v_4 intr_alt_rate_mag) 0) (= ?v_4 0))) (not (and (<= 0 (+ (/ 823 10000) ?v_13)) (or (and (< 0 (+ 0 ?v_1 ?v_5)) (<= 0 (+ 100 ?v_6 ?v_3))) (and (<= 0 (+ 0 ?v_6 ?v_3)) (<= 0 (+ 100 ?v_1 ?v_5)))))) (or (and ?v_7 ?v_10 ?v_9) (and ?v_8 ?v_9 ?v_12) (and ?v_10 ?v_11 ?v_12)) (ite (< 0 (+ (/ (- 1) 720) ?v_16)) (= (+ 0 (* (- 1) (* ?v_14 ?v_0)) ?v_13) 0) (= (+ 0 ?v_14 (* (- 720) ?v_15)) 0)) (= (and (< 0 ?v_16) (<= 0 (+ 0 (* (- 1) ?v_14) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_21 ?v_22 ?v_1 ?v_5)) (< 0 (+ 500 ?v_19 ?v_20 ?v_6 ?v_3))) (and (< 0 (+ 0 ?v_19 ?v_20 ?v_6 ?v_3)) (< 0 (+ 500 ?v_21 ?v_22 ?v_1 ?v_5))))) ?v_23)) (and (< 0 rrm) (< 0 (+ (/ 1 3) (* (- 1) rrm))) (<= 0 intr_alt_rate_mag) (<= 0 (+ 100 (* (- 1) intr_alt_rate_mag))) (<= 0 own_alt_rate_mag) (<= 0 (+ 100 (* (- 1) own_alt_rate_mag))) (<= 0 own_target_alt) (<= 0 (+ 30000 ?v_24)) (<= 0 ?v_3) (<= 0 (+ 30000 ?v_5))))))))))
(assert (let ((?v_14 (own_alt 0)) (?v_17 (state_is_No_RA 0)) (?v_9 (own_alt_rate 0)) (?v_3 (intr_alt 0)) (?v_29 (state_is_Climb 0)) (?v_24 (range 1)) (?v_0 (range_rate 1)) (?v_5 (intr_alt 1)) (?v_6 (intr_alt_rate 1)) (?v_7 (own_alt 1)) (?v_8 (own_alt_rate 1))) (let ((?v_10 (= ?v_8 ?v_9)) (?v_13 (alt_proj 1)) (?v_16 (limited_alt_proj 1)) (?v_20 (state_is_No_RA 1)) (?v_18 (state_is_Climb 1))) (let ((?v_22 (not ?v_18)) (?v_21 (state_is_Descend 1))) (let ((?v_19 (not ?v_21)) (?v_23 (not ?v_20)) (?v_25 (tau 1)) (?v_26 (Collision_Threat 1)) (?v_31 (* ?v_0 ?v_24))) (let ((?v_33 (* ?v_25 ?v_8))) (let ((?v_37 (* 1 ?v_33)) (?v_34 (* ?v_25 ?v_6))) (let ((?v_36 (* 1 ?v_34)) (?v_12 (* (- 1) ?v_14)) (?v_15 (* (- 1) own_target_alt)) (?v_1 (* (- 1) ?v_3)) (?v_4 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_27 (* (- 1) ?v_5)) (?v_28 (* (- 1) ?v_7)) (?v_11 (* (- 1) ?v_9)) (?v_32 (* (- 1) ?v_0)) (?v_30 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_31)))) (?v_38 (* (- 1) ?v_34)) (?v_35 (* (- 1) ?v_33))) (and (and (= (+ 0 ?v_24 (* (- 1) (range 0)) (* (- 1) (range_rate 0))) 0) (ite (< 0 (+ (- 1) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 ?v_1 intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_5 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_4)) (< 0 (+ 0 ?v_3 ?v_2 ?v_4))) (= (+ 0 ?v_5 ?v_1 intr_alt_rate_mag) 0) (= ?v_5 intr_target_alt))) (ite (< 0 (+ 0 ?v_27 intr_target_alt)) (= ?v_6 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_5 ?v_4)) (= ?v_6 ?v_2) (= ?v_6 0))) (ite ?v_17 (ite (< 0 (+ 0 ?v_28 own_target_alt)) (= ?v_8 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_7 ?v_15)) (= ?v_8 (* (- 1) own_alt_rate_mag)) (= ?v_8 0))) (ite ?v_29 (ite (<= 0 (+ 25 ?v_11)) (= ?v_8 25) ?v_10) (ite (<= 0 (+ 25 ?v_9)) (= ?v_8 (- 25)) ?v_10))) (= (+ 0 ?v_13 ?v_11 ?v_12) 0) (ite (or (and (< 0 (+ 0 ?v_12 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_13) own_target_alt))) (and (< 0 (+ 0 ?v_14 ?v_15)) (< 0 (+ 0 ?v_13 ?v_15)))) (= ?v_16 ?v_13) (= ?v_16 own_target_alt)) (ite ?v_17 (= ?v_16 ?v_7) (= ?v_13 ?v_7)) (or (and ?v_20 ?v_22 ?v_19) (and ?v_18 ?v_19 ?v_23) (and ?v_21 ?v_22 ?v_23)) (ite (< 0 (+ (/ (- 1) 720) ?v_32)) (= (+ 0 (* 1 (* ?v_25 ?v_0)) ?v_24) 0) (= (+ 0 ?v_25 (* (- 720) ?v_24)) 0)) (or (not ?v_17) (and (not ?v_26) ?v_20) (and ?v_26 ?v_18 (< 0 (+ 0 ?v_7 ?v_27))) (and ?v_26 ?v_21 (<= 0 (+ 0 ?v_28 ?v_5)))) (or ?v_17 (and ?v_29 ?v_18 ?v_30) (and (state_is_Descend 0) ?v_21 ?v_30) (and ?v_20 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_31)))))) (= (and (< 0 ?v_32) (<= 0 (+ 0 (* (- 1) ?v_25) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_37 ?v_38 ?v_7 ?v_27)) (< 0 (+ 500 ?v_35 ?v_36 ?v_28 ?v_5))) (and (< 0 (+ 0 ?v_35 ?v_36 ?v_28 ?v_5)) (< 0 (+ 500 ?v_37 ?v_38 ?v_7 ?v_27))))) ?v_26))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 1)) (?v_15 (own_alt 1)) (?v_10 (own_alt_rate 1)) (?v_18 (state_is_No_RA 1)) (?v_30 (state_is_Climb 1)) (?v_25 (range 2)) (?v_0 (range_rate 2)) (?v_6 (intr_alt 2)) (?v_7 (intr_alt_rate 2)) (?v_8 (own_alt 2)) (?v_9 (own_alt_rate 2))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 2)) (?v_17 (limited_alt_proj 2)) (?v_21 (state_is_No_RA 2)) (?v_19 (state_is_Climb 2))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 2))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 2)) (?v_27 (Collision_Threat 2)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 1)) (* (- 1) (range 1))) 0) (ite (< 0 (+ (- 2) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 1) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 2)) (?v_15 (own_alt 2)) (?v_10 (own_alt_rate 2)) (?v_18 (state_is_No_RA 2)) (?v_30 (state_is_Climb 2)) (?v_25 (range 3)) (?v_0 (range_rate 3)) (?v_6 (intr_alt 3)) (?v_7 (intr_alt_rate 3)) (?v_8 (own_alt 3)) (?v_9 (own_alt_rate 3))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 3)) (?v_17 (limited_alt_proj 3)) (?v_21 (state_is_No_RA 3)) (?v_19 (state_is_Climb 3))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 3))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 3)) (?v_27 (Collision_Threat 3)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 2)) (* (- 1) (range 2))) 0) (ite (< 0 (+ (- 3) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 2) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 3)) (?v_15 (own_alt 3)) (?v_10 (own_alt_rate 3)) (?v_18 (state_is_No_RA 3)) (?v_30 (state_is_Climb 3)) (?v_25 (range 4)) (?v_0 (range_rate 4)) (?v_6 (intr_alt 4)) (?v_7 (intr_alt_rate 4)) (?v_8 (own_alt 4)) (?v_9 (own_alt_rate 4))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 4)) (?v_17 (limited_alt_proj 4)) (?v_21 (state_is_No_RA 4)) (?v_19 (state_is_Climb 4))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 4))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 4)) (?v_27 (Collision_Threat 4)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 3)) (* (- 1) (range 3))) 0) (ite (< 0 (+ (- 4) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 3) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 4)) (?v_15 (own_alt 4)) (?v_10 (own_alt_rate 4)) (?v_18 (state_is_No_RA 4)) (?v_30 (state_is_Climb 4)) (?v_25 (range 5)) (?v_0 (range_rate 5)) (?v_6 (intr_alt 5)) (?v_7 (intr_alt_rate 5)) (?v_8 (own_alt 5)) (?v_9 (own_alt_rate 5))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 5)) (?v_17 (limited_alt_proj 5)) (?v_21 (state_is_No_RA 5)) (?v_19 (state_is_Climb 5))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 5))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 5)) (?v_27 (Collision_Threat 5)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 4)) (* (- 1) (range 4))) 0) (ite (< 0 (+ (- 5) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 4) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 5)) (?v_15 (own_alt 5)) (?v_10 (own_alt_rate 5)) (?v_18 (state_is_No_RA 5)) (?v_30 (state_is_Climb 5)) (?v_25 (range 6)) (?v_0 (range_rate 6)) (?v_6 (intr_alt 6)) (?v_7 (intr_alt_rate 6)) (?v_8 (own_alt 6)) (?v_9 (own_alt_rate 6))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 6)) (?v_17 (limited_alt_proj 6)) (?v_21 (state_is_No_RA 6)) (?v_19 (state_is_Climb 6))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 6))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 6)) (?v_27 (Collision_Threat 6)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 5)) (* (- 1) (range 5))) 0) (ite (< 0 (+ (- 6) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 5) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 6)) (?v_15 (own_alt 6)) (?v_10 (own_alt_rate 6)) (?v_18 (state_is_No_RA 6)) (?v_30 (state_is_Climb 6)) (?v_25 (range 7)) (?v_0 (range_rate 7)) (?v_6 (intr_alt 7)) (?v_7 (intr_alt_rate 7)) (?v_8 (own_alt 7)) (?v_9 (own_alt_rate 7))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 7)) (?v_17 (limited_alt_proj 7)) (?v_21 (state_is_No_RA 7)) (?v_19 (state_is_Climb 7))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 7))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 7)) (?v_27 (Collision_Threat 7)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 6)) (* (- 1) (range 6))) 0) (ite (< 0 (+ (- 7) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 6) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 7)) (?v_15 (own_alt 7)) (?v_10 (own_alt_rate 7)) (?v_18 (state_is_No_RA 7)) (?v_30 (state_is_Climb 7)) (?v_25 (range 8)) (?v_0 (range_rate 8)) (?v_6 (intr_alt 8)) (?v_7 (intr_alt_rate 8)) (?v_8 (own_alt 8)) (?v_9 (own_alt_rate 8))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 8)) (?v_17 (limited_alt_proj 8)) (?v_21 (state_is_No_RA 8)) (?v_19 (state_is_Climb 8))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 8))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 8)) (?v_27 (Collision_Threat 8)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 7)) (* (- 1) (range 7))) 0) (ite (< 0 (+ (- 8) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 7) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 8)) (?v_15 (own_alt 8)) (?v_10 (own_alt_rate 8)) (?v_18 (state_is_No_RA 8)) (?v_30 (state_is_Climb 8)) (?v_25 (range 9)) (?v_0 (range_rate 9)) (?v_6 (intr_alt 9)) (?v_7 (intr_alt_rate 9)) (?v_8 (own_alt 9)) (?v_9 (own_alt_rate 9))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 9)) (?v_17 (limited_alt_proj 9)) (?v_21 (state_is_No_RA 9)) (?v_19 (state_is_Climb 9))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 9))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 9)) (?v_27 (Collision_Threat 9)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 8)) (* (- 1) (range 8))) 0) (ite (< 0 (+ (- 9) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 8) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (let ((?v_3 (intr_alt 0)) (?v_4 (intr_alt 9)) (?v_15 (own_alt 9)) (?v_10 (own_alt_rate 9)) (?v_18 (state_is_No_RA 9)) (?v_30 (state_is_Climb 9)) (?v_25 (range 10)) (?v_0 (range_rate 10)) (?v_6 (intr_alt 10)) (?v_7 (intr_alt_rate 10)) (?v_8 (own_alt 10)) (?v_9 (own_alt_rate 10))) (let ((?v_11 (= ?v_9 ?v_10)) (?v_14 (alt_proj 10)) (?v_17 (limited_alt_proj 10)) (?v_21 (state_is_No_RA 10)) (?v_19 (state_is_Climb 10))) (let ((?v_23 (not ?v_19)) (?v_22 (state_is_Descend 10))) (let ((?v_20 (not ?v_22)) (?v_24 (not ?v_21)) (?v_26 (tau 10)) (?v_27 (Collision_Threat 10)) (?v_32 (* ?v_0 ?v_25))) (let ((?v_34 (* ?v_26 ?v_9))) (let ((?v_38 (* 1 ?v_34)) (?v_35 (* ?v_26 ?v_7))) (let ((?v_37 (* 1 ?v_35)) (?v_16 (* (- 1) own_target_alt)) (?v_5 (* (- 1) intr_target_alt)) (?v_2 (* (- 1) intr_alt_rate_mag)) (?v_1 (* (- 1) ?v_4)) (?v_13 (* (- 1) ?v_15)) (?v_28 (* (- 1) ?v_6)) (?v_29 (* (- 1) ?v_8)) (?v_12 (* (- 1) ?v_10)) (?v_33 (* (- 1) ?v_0)) (?v_31 (<= 0 (+ (/ 1 3600) (* (- 1) ?v_32)))) (?v_39 (* (- 1) ?v_35)) (?v_36 (* (- 1) ?v_34))) (and (and (= (+ 0 ?v_25 (* (- 1) (range_rate 9)) (* (- 1) (range 9))) 0) (ite (< 0 (+ (- 10) TCA)) (= ?v_0 (* (- 1) rrm)) (= ?v_0 rrm)) (ite (and (< 0 (+ 0 (* (- 1) ?v_3) intr_target_alt)) (< 0 (+ 0 ?v_1 ?v_2 intr_target_alt))) (= (+ 0 ?v_6 ?v_1 ?v_2) 0) (ite (and (<= 0 (+ 0 ?v_3 ?v_5)) (< 0 (+ 0 ?v_4 ?v_2 ?v_5))) (= (+ 0 ?v_6 ?v_1 intr_alt_rate_mag) 0) (= ?v_6 intr_target_alt))) (ite (< 0 (+ 0 ?v_28 intr_target_alt)) (= ?v_7 intr_alt_rate_mag) (ite (< 0 (+ 0 ?v_6 ?v_5)) (= ?v_7 ?v_2) (= ?v_7 0))) (ite ?v_18 (ite (< 0 (+ 0 ?v_29 own_target_alt)) (= ?v_9 own_alt_rate_mag) (ite (< 0 (+ 0 ?v_8 ?v_16)) (= ?v_9 (* (- 1) own_alt_rate_mag)) (= ?v_9 0))) (ite ?v_30 (ite (<= 0 (+ 25 ?v_12)) (= ?v_9 25) ?v_11) (ite (<= 0 (+ 25 ?v_10)) (= ?v_9 (- 25)) ?v_11))) (= (+ 0 ?v_14 ?v_12 ?v_13) 0) (ite (or (and (< 0 (+ 0 ?v_13 own_target_alt)) (< 0 (+ 0 (* (- 1) ?v_14) own_target_alt))) (and (< 0 (+ 0 ?v_15 ?v_16)) (< 0 (+ 0 ?v_14 ?v_16)))) (= ?v_17 ?v_14) (= ?v_17 own_target_alt)) (ite ?v_18 (= ?v_17 ?v_8) (= ?v_14 ?v_8)) (or (and ?v_21 ?v_23 ?v_20) (and ?v_19 ?v_20 ?v_24) (and ?v_22 ?v_23 ?v_24)) (ite (< 0 (+ (/ (- 1) 720) ?v_33)) (= (+ 0 (* 1 (* ?v_26 ?v_0)) ?v_25) 0) (= (+ 0 ?v_26 (* (- 720) ?v_25)) 0)) (or (not ?v_18) (and (not ?v_27) ?v_21) (and ?v_27 ?v_19 (< 0 (+ 0 ?v_8 ?v_28))) (and ?v_27 ?v_22 (<= 0 (+ 0 ?v_29 ?v_6)))) (or ?v_18 (and ?v_30 ?v_19 ?v_31) (and (state_is_Descend 9) ?v_22 ?v_31) (and ?v_21 (< 0 (+ (/ (- 1) 3600) (* 1 ?v_32)))))) (= (and (< 0 ?v_33) (<= 0 (+ 0 (* (- 1) ?v_26) MAX_Tau_To_Trigger_Threat)) (or (and (<= 0 (+ 0 ?v_38 ?v_39 ?v_8 ?v_28)) (< 0 (+ 500 ?v_36 ?v_37 ?v_29 ?v_6))) (and (< 0 (+ 0 ?v_36 ?v_37 ?v_29 ?v_6)) (< 0 (+ 500 ?v_38 ?v_39 ?v_8 ?v_28))))) ?v_27))))))))))
(assert (= (+ 5 (* (- 1) TCA)) 0))
(assert (= (+ 4 (* (- 1) MAX_Tau_To_Trigger_Threat)) 0))
(assert (let ((?v_0 (own_alt 0)) (?v_1 (intr_alt 0)) (?v_5 (intr_alt 1)) (?v_4 (own_alt 1)) (?v_9 (intr_alt 2)) (?v_8 (own_alt 2)) (?v_13 (intr_alt 3)) (?v_12 (own_alt 3)) (?v_17 (intr_alt 4)) (?v_16 (own_alt 4)) (?v_21 (intr_alt 5)) (?v_20 (own_alt 5)) (?v_25 (intr_alt 6)) (?v_24 (own_alt 6)) (?v_29 (intr_alt 7)) (?v_28 (own_alt 7)) (?v_33 (intr_alt 8)) (?v_32 (own_alt 8)) (?v_37 (intr_alt 9)) (?v_36 (own_alt 9)) (?v_41 (intr_alt 10)) (?v_40 (own_alt 10))) (let ((?v_2 (* (- 1) ?v_0)) (?v_3 (* (- 1) ?v_1)) (?v_7 (* (- 1) ?v_5)) (?v_6 (* (- 1) ?v_4)) (?v_11 (* (- 1) ?v_9)) (?v_10 (* (- 1) ?v_8)) (?v_15 (* (- 1) ?v_13)) (?v_14 (* (- 1) ?v_12)) (?v_19 (* (- 1) ?v_17)) (?v_18 (* (- 1) ?v_16)) (?v_23 (* (- 1) ?v_21)) (?v_22 (* (- 1) ?v_20)) (?v_27 (* (- 1) ?v_25)) (?v_26 (* (- 1) ?v_24)) (?v_31 (* (- 1) ?v_29)) (?v_30 (* (- 1) ?v_28)) (?v_35 (* (- 1) ?v_33)) (?v_34 (* (- 1) ?v_32)) (?v_39 (* (- 1) ?v_37)) (?v_38 (* (- 1) ?v_36)) (?v_43 (* (- 1) ?v_41)) (?v_42 (* (- 1) ?v_40))) (or (or (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 0)))) (or (and (< 0 (+ 0 ?v_0 ?v_3)) (<= 0 (+ 100 ?v_2 ?v_1))) (and (<= 0 (+ 0 ?v_2 ?v_1)) (<= 0 (+ 100 ?v_0 ?v_3))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 1)))) (or (and (< 0 (+ 0 ?v_4 ?v_7)) (<= 0 (+ 100 ?v_6 ?v_5))) (and (<= 0 (+ 0 ?v_6 ?v_5)) (<= 0 (+ 100 ?v_4 ?v_7))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 2)))) (or (and (< 0 (+ 0 ?v_8 ?v_11)) (<= 0 (+ 100 ?v_10 ?v_9))) (and (<= 0 (+ 0 ?v_10 ?v_9)) (<= 0 (+ 100 ?v_8 ?v_11))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 3)))) (or (and (< 0 (+ 0 ?v_12 ?v_15)) (<= 0 (+ 100 ?v_14 ?v_13))) (and (<= 0 (+ 0 ?v_14 ?v_13)) (<= 0 (+ 100 ?v_12 ?v_15))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 4)))) (or (and (< 0 (+ 0 ?v_16 ?v_19)) (<= 0 (+ 100 ?v_18 ?v_17))) (and (<= 0 (+ 0 ?v_18 ?v_17)) (<= 0 (+ 100 ?v_16 ?v_19))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 5)))) (or (and (< 0 (+ 0 ?v_20 ?v_23)) (<= 0 (+ 100 ?v_22 ?v_21))) (and (<= 0 (+ 0 ?v_22 ?v_21)) (<= 0 (+ 100 ?v_20 ?v_23))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 6)))) (or (and (< 0 (+ 0 ?v_24 ?v_27)) (<= 0 (+ 100 ?v_26 ?v_25))) (and (<= 0 (+ 0 ?v_26 ?v_25)) (<= 0 (+ 100 ?v_24 ?v_27))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 7)))) (or (and (< 0 (+ 0 ?v_28 ?v_31)) (<= 0 (+ 100 ?v_30 ?v_29))) (and (<= 0 (+ 0 ?v_30 ?v_29)) (<= 0 (+ 100 ?v_28 ?v_31))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 8)))) (or (and (< 0 (+ 0 ?v_32 ?v_35)) (<= 0 (+ 100 ?v_34 ?v_33))) (and (<= 0 (+ 0 ?v_34 ?v_33)) (<= 0 (+ 100 ?v_32 ?v_35))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 9)))) (or (and (< 0 (+ 0 ?v_36 ?v_39)) (<= 0 (+ 100 ?v_38 ?v_37))) (and (<= 0 (+ 0 ?v_38 ?v_37)) (<= 0 (+ 100 ?v_36 ?v_39)))))) (and (<= 0 (+ (/ 823 10000) (* (- 1) (range 10)))) (or (and (< 0 (+ 0 ?v_40 ?v_43)) (<= 0 (+ 100 ?v_42 ?v_41))) (and (<= 0 (+ 0 ?v_42 ?v_41)) (<= 0 (+ 100 ?v_40 ?v_43)))))))))
(check-sat)
(exit)
